a:Id, T:Type, ds:x:Id fp Type, P:(State(ds)TProp).
(with ds: ds action a:T precondition a(v) is P s v)  MsgA 

latex

Definitions

False, Unit, T, P  Q, P  Q, P  Q, P  Q, , p  q, true, A, b, True, b, P & Q, x  dom(f), f(x), p  q, eqof(d), false, (x  l), if b t else f fi, Top, x. t(x), MsgA, a:A fp B(a), (with ds: ds action a:T precondition a(v) is P s v), mk-ma, S  T, Prop, S  T, State(ds), IdDeq, Valtype(da;k), 1of(t), x : v, locl(a), f(x)?z, KindDeq, rcv(l,tg), 2of(t), , x:A. B(x), Id, IdLnk, t  T, Knd

Lemmas

fpf-empty wf, pi2 wf, rcv wf, Kind-deq wf, fpf-cap wf, pi1 wf, ma-valtype wf, IdLnk wf, id-deq wf, ma-state wf, locl wf, fpf-single wf, Knd wf, mk-ma wf, Id wf, fpf wf, top wf, bfalse wf, eqof wf, bor wf, ifthenelse wf, l member wf, assert wf, bnot wf, not wf, btrue wf, band wf, bool wf, assert of bnot, and functionality wrt iff, assert of band, iff transitivity, bnot thru bor, true wf, squash wf, eqff to assert, assert of bor, eqtt to assert, false wf, nil member, or functionality wrt iff, cons member, deq property